Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PlusSwap

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 175 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load668(i78, i84, i80) → Cond_Load668(i84 > 0 && i80 + 1 > 0, i78, i84, i80)
Cond_Load668(TRUE, i78, i84, i80) → Load668(i84 - 1, i78, i80 + 1)
The set Q consists of the following terms:
Load668(x0, x1, x2)
Cond_Load668(TRUE, x0, x1, x2)

(5) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load668(i78, i84, i80) → Cond_Load668(i84 > 0 && i80 + 1 > 0, i78, i84, i80)
Cond_Load668(TRUE, i78, i84, i80) → Load668(i84 - 1, i78, i80 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(i84[0] > 0 && i80[0] + 1 > 0, i78[0], i84[0], i80[0])
(1): COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(i84[1] - 1, i78[1], i80[1] + 1)

(0) -> (1), if ((i84[0] > 0 && i80[0] + 1 > 0 →^* TRUE)∧(i84[0] →^* i84[1])∧(i80[0] →^* i80[1])∧(i78[0] →^* i78[1]))

(1) -> (0), if ((i80[1] + 1 →^* i80[0])∧(i78[1] →^* i84[0])∧(i84[1] - 1 →^* i78[0]))

The set Q consists of the following terms:
Load668(x0, x1, x2)
Cond_Load668(TRUE, x0, x1, x2)

(7) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(i84[0] > 0 && i80[0] + 1 > 0, i78[0], i84[0], i80[0])
(1): COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(i84[1] - 1, i78[1], i80[1] + 1)

(0) -> (1), if ((i84[0] > 0 && i80[0] + 1 > 0 →^* TRUE)∧(i84[0] →^* i84[1])∧(i80[0] →^* i80[1])∧(i78[0] →^* i78[1]))

(1) -> (0), if ((i80[1] + 1 →^* i80[0])∧(i78[1] →^* i84[0])∧(i84[1] - 1 →^* i78[0]))

The set Q consists of the following terms:
Load668(x0, x1, x2)
Cond_Load668(TRUE, x0, x1, x2)

(9) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD668(i78, i84, i80) → COND_LOAD668(&&(>(i84, 0), >(+(i80, 1), 0)), i78, i84, i80) the following chains were created:

• We consider the chain LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0]), COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1)) which results in the following constraint:
  

  (1)    (&&(>(i84[0], 0), >(+(i80[0], 1), 0))=TRUE∧i84[0]=i84[1]∧i80[0]=i80[1]∧i78[0]=i78[1] ⇒ LOAD668(i78[0], i84[0], i80[0])≥NonInfC∧LOAD668(i78[0], i84[0], i80[0])≥COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])∧(U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥))

  
  
  We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>(i84[0], 0)=TRUE∧>(+(i80[0], 1), 0)=TRUE ⇒ LOAD668(i78[0], i84[0], i80[0])≥NonInfC∧LOAD668(i78[0], i84[0], i80[0])≥COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])∧(U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] + [bni_14]i78[0] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] + [bni_14]i78[0] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] + [bni_14]i78[0] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (6)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14] = 0∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (i84[0] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14] = 0∧[(2)bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

  
  
  

For Pair COND_LOAD668(TRUE, i78, i84, i80) → LOAD668(-(i84, 1), i78, +(i80, 1)) the following chains were created:

• We consider the chain LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0]), COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1)), LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0]), COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1)), LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0]), COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1)) which results in the following constraint:
  

  (8)    (&&(>(i84[0], 0), >(+(i80[0], 1), 0))=TRUE∧i84[0]=i84[1]∧i80[0]=i80[1]∧i78[0]=i78[1]∧+(i80[1], 1)=i80[0]1∧i78[1]=i84[0]1∧-(i84[1], 1)=i78[0]1∧&&(>(i84[0]1, 0), >(+(i80[0]1, 1), 0))=TRUE∧i84[0]1=i84[1]1∧i80[0]1=i80[1]1∧i78[0]1=i78[1]1∧+(i80[1]1, 1)=i80[0]2∧i78[1]1=i84[0]2∧-(i84[1]1, 1)=i78[0]2∧&&(>(i84[0]2, 0), >(+(i80[0]2, 1), 0))=TRUE∧i84[0]2=i84[1]2∧i80[0]2=i80[1]2∧i78[0]2=i78[1]2 ⇒ COND_LOAD668(TRUE, i78[1]1, i84[1]1, i80[1]1)≥NonInfC∧COND_LOAD668(TRUE, i78[1]1, i84[1]1, i80[1]1)≥LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))∧(U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥))

  
  
  We simplified constraint (8) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (9)    (>(i84[0], 0)=TRUE∧>(+(i80[0], 1), 0)=TRUE∧>(i84[0]1, 0)=TRUE∧>(+(+(i80[0], 1), 1), 0)=TRUE∧>(-(i84[0], 1), 0)=TRUE∧>(+(+(+(i80[0], 1), 1), 1), 0)=TRUE ⇒ COND_LOAD668(TRUE, -(i84[0], 1), i84[0]1, +(i80[0], 1))≥NonInfC∧COND_LOAD668(TRUE, -(i84[0], 1), i84[0]1, +(i80[0], 1))≥LOAD668(-(i84[0]1, 1), -(i84[0], 1), +(+(i80[0], 1), 1))∧(U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥))

  
  
  We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (10)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0∧i84[0]1 + [-1] ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] + [-2] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (11)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0∧i84[0]1 + [-1] ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] + [-2] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (12)    (i84[0] + [-1] ≥ 0∧i80[0] ≥ 0∧i84[0]1 + [-1] ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] + [-2] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (13)    (i84[0] ≥ 0∧i80[0] ≥ 0∧i84[0]1 + [-1] ≥ 0∧i80[0] + [1] ≥ 0∧[-1] + i84[0] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)Bound*bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (14)    ([1] + i84[0] ≥ 0∧i80[0] ≥ 0∧i84[0]1 + [-1] ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[bni_16 + (-1)Bound*bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (15)    ([1] + i84[0] ≥ 0∧i80[0] ≥ 0∧i84[0]1 ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] ≥ 0∧i80[0] + [2] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)Bound*bni_16 + (2)bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  We simplified constraint (15) using rule (IDP_POLY_GCD) which results in the following new constraint:
  

  (16)    ([1] + i84[0] ≥ 0∧i80[0] ≥ 0∧i84[0]1 ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] ≥ 0∧[1] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)Bound*bni_16 + (2)bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• LOAD668(i78, i84, i80) → COND_LOAD668(&&(>(i84, 0), >(+(i80, 1), 0)), i78, i84, i80)
  
  • (i84[0] ≥ 0∧i80[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])), ≥)∧[bni_14] = 0∧[(2)bni_14 + (-1)Bound*bni_14] + [bni_14]i84[0] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)
    
  
  
• COND_LOAD668(TRUE, i78, i84, i80) → LOAD668(-(i84, 1), i78, +(i80, 1))
  
  • ([1] + i84[0] ≥ 0∧i80[0] ≥ 0∧i84[0]1 ≥ 0∧i80[0] + [1] ≥ 0∧i84[0] ≥ 0∧[1] ≥ 0 ⇒ (U^Increasing(LOAD668(-(i84[1]1, 1), i78[1]1, +(i80[1]1, 1))), ≥)∧[(-1)Bound*bni_16 + (2)bni_16] + [bni_16]i84[0]1 + [bni_16]i84[0] ≥ 0∧[(-1)bso_17] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = [2]   
POL(FALSE) = [2]   
POL(LOAD668(x₁, x₂, x₃)) = [1] + x₂ + x₁   
POL(COND_LOAD668(x₁, x₂, x₃, x₄)) = [2] + x₃ + x₂ + [-1]x₁   
POL(&&(x₁, x₂)) = [2]   
POL(>(x₁, x₂)) = [-1]   
POL(0) = 0   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   

The following pairs are in P_>:

LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(&&(>(i84[0], 0), >(+(i80[0], 1), 0)), i78[0], i84[0], i80[0])

The following pairs are in P_bound:

COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1))

The following pairs are in P_≥:

COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(-(i84[1], 1), i78[1], +(i80[1], 1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ ↔ TRUE¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
&&(FALSE, FALSE)¹ ↔ FALSE¹

(10) Complex Obligation (AND)

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD668(TRUE, i78[1], i84[1], i80[1]) → LOAD668(i84[1] - 1, i78[1], i80[1] + 1)


The set Q consists of the following terms:
Load668(x0, x1, x2)
Cond_Load668(TRUE, x0, x1, x2)

(12) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(13) TRUE

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD668(i78[0], i84[0], i80[0]) → COND_LOAD668(i84[0] > 0 && i80[0] + 1 > 0, i78[0], i84[0], i80[0])


The set Q consists of the following terms:
Load668(x0, x1, x2)
Cond_Load668(TRUE, x0, x1, x2)

(15) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(16) TRUE